0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 84 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 15 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 9 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPOrderProof (⇔, 0 ms)
↳29 QDP
↳30 DependencyGraphProof (⇔, 0 ms)
↳31 TRUE
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
DIVD_IN_GGA(T7, s(T8), T10) → U7_GGA(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
DIVD_IN_GGA(T7, s(T8), T10) → DIV_SB_IN_GGA(T7, T8, T10)
DIV_SB_IN_GGA(s(T24), T25, 0) → U2_GGA(T24, T25, lssA_in_gg(T24, T25))
DIV_SB_IN_GGA(s(T24), T25, 0) → LSSA_IN_GG(T24, T25)
LSSA_IN_GG(s(T36), s(T37)) → U1_GG(T36, T37, lssA_in_gg(T36, T37))
LSSA_IN_GG(s(T36), s(T37)) → LSSA_IN_GG(T36, T37)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U3_GGA(T49, T50, T52, subC_in_gga(T49, T50, X49))
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → SUBC_IN_GGA(T49, T50, X49)
SUBC_IN_GGA(s(T66), s(T67), X77) → U6_GGA(T66, T67, X77, subC_in_gga(T66, T67, X77))
SUBC_IN_GGA(s(T66), s(T67), X77) → SUBC_IN_GGA(T66, T67, X77)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_GGA(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
DIVD_IN_GGA(T7, s(T8), T10) → U7_GGA(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
DIVD_IN_GGA(T7, s(T8), T10) → DIV_SB_IN_GGA(T7, T8, T10)
DIV_SB_IN_GGA(s(T24), T25, 0) → U2_GGA(T24, T25, lssA_in_gg(T24, T25))
DIV_SB_IN_GGA(s(T24), T25, 0) → LSSA_IN_GG(T24, T25)
LSSA_IN_GG(s(T36), s(T37)) → U1_GG(T36, T37, lssA_in_gg(T36, T37))
LSSA_IN_GG(s(T36), s(T37)) → LSSA_IN_GG(T36, T37)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U3_GGA(T49, T50, T52, subC_in_gga(T49, T50, X49))
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → SUBC_IN_GGA(T49, T50, X49)
SUBC_IN_GGA(s(T66), s(T67), X77) → U6_GGA(T66, T67, X77, subC_in_gga(T66, T67, X77))
SUBC_IN_GGA(s(T66), s(T67), X77) → SUBC_IN_GGA(T66, T67, X77)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_GGA(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
SUBC_IN_GGA(s(T66), s(T67), X77) → SUBC_IN_GGA(T66, T67, X77)
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
SUBC_IN_GGA(s(T66), s(T67), X77) → SUBC_IN_GGA(T66, T67, X77)
SUBC_IN_GGA(s(T66), s(T67)) → SUBC_IN_GGA(T66, T67)
From the DPs we obtained the following set of size-change graphs:
LSSA_IN_GG(s(T36), s(T37)) → LSSA_IN_GG(T36, T37)
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
LSSA_IN_GG(s(T36), s(T37)) → LSSA_IN_GG(T36, T37)
LSSA_IN_GG(s(T36), s(T37)) → LSSA_IN_GG(T36, T37)
From the DPs we obtained the following set of size-change graphs:
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
divD_in_gga(T7, s(T8), T10) → U7_gga(T7, T8, T10, div_sB_in_gga(T7, T8, T10))
div_sB_in_gga(0, T15, 0) → div_sB_out_gga(0, T15, 0)
div_sB_in_gga(s(T24), T25, 0) → U2_gga(T24, T25, lssA_in_gg(T24, T25))
lssA_in_gg(s(T36), s(T37)) → U1_gg(T36, T37, lssA_in_gg(T36, T37))
lssA_in_gg(0, s(T42)) → lssA_out_gg(0, s(T42))
U1_gg(T36, T37, lssA_out_gg(T36, T37)) → lssA_out_gg(s(T36), s(T37))
U2_gga(T24, T25, lssA_out_gg(T24, T25)) → div_sB_out_gga(s(T24), T25, 0)
div_sB_in_gga(s(T49), T50, s(T52)) → U3_gga(T49, T50, T52, subC_in_gga(T49, T50, X49))
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
U3_gga(T49, T50, T52, subC_out_gga(T49, T50, X49)) → div_sB_out_gga(s(T49), T50, s(T52))
div_sB_in_gga(s(T49), T50, s(T52)) → U4_gga(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_gga(T49, T50, T52, subC_out_gga(T49, T50, T55)) → U5_gga(T49, T50, T52, div_sB_in_gga(T55, T50, T52))
U5_gga(T49, T50, T52, div_sB_out_gga(T55, T50, T52)) → div_sB_out_gga(s(T49), T50, s(T52))
U7_gga(T7, T8, T10, div_sB_out_gga(T7, T8, T10)) → divD_out_gga(T7, s(T8), T10)
DIV_SB_IN_GGA(s(T49), T50, s(T52)) → U4_GGA(T49, T50, T52, subC_in_gga(T49, T50, T55))
U4_GGA(T49, T50, T52, subC_out_gga(T49, T50, T55)) → DIV_SB_IN_GGA(T55, T50, T52)
subC_in_gga(s(T66), s(T67), X77) → U6_gga(T66, T67, X77, subC_in_gga(T66, T67, X77))
subC_in_gga(T72, 0, T72) → subC_out_gga(T72, 0, T72)
U6_gga(T66, T67, X77, subC_out_gga(T66, T67, X77)) → subC_out_gga(s(T66), s(T67), X77)
DIV_SB_IN_GGA(s(T49), T50) → U4_GGA(T50, subC_in_gga(T49, T50))
U4_GGA(T50, subC_out_gga(T55)) → DIV_SB_IN_GGA(T55, T50)
subC_in_gga(s(T66), s(T67)) → U6_gga(subC_in_gga(T66, T67))
subC_in_gga(T72, 0) → subC_out_gga(T72)
U6_gga(subC_out_gga(X77)) → subC_out_gga(X77)
subC_in_gga(x0, x1)
U6_gga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV_SB_IN_GGA(s(T49), T50) → U4_GGA(T50, subC_in_gga(T49, T50))
POL(0) = 0
POL(DIV_SB_IN_GGA(x1, x2)) = x1
POL(U4_GGA(x1, x2)) = x2
POL(U6_gga(x1)) = 1 + x1
POL(s(x1)) = 1 + x1
POL(subC_in_gga(x1, x2)) = x1
POL(subC_out_gga(x1)) = x1
subC_in_gga(s(T66), s(T67)) → U6_gga(subC_in_gga(T66, T67))
subC_in_gga(T72, 0) → subC_out_gga(T72)
U6_gga(subC_out_gga(X77)) → subC_out_gga(X77)
U4_GGA(T50, subC_out_gga(T55)) → DIV_SB_IN_GGA(T55, T50)
subC_in_gga(s(T66), s(T67)) → U6_gga(subC_in_gga(T66, T67))
subC_in_gga(T72, 0) → subC_out_gga(T72)
U6_gga(subC_out_gga(X77)) → subC_out_gga(X77)
subC_in_gga(x0, x1)
U6_gga(x0)